Secure two-party computation enables two parties to compute a function f over their joint, private inputs x and y, respectively. Neither party can infer anything about the other party's input (e.g., y) except what can be inferred from one's own input (e.g., x) and the of the computation output (e.g., f(x, y)).
Secure computation has many applications (e.g., in the financial sector) and has been successfully deployed in commercial and industrial settings. Secure computation protocols, however, are notoriously difficult to implement. For example, secure computation protocols can encompass arbitrary functionality in the joint computation. As another example, secure computation protocols follow a rigorous approach to security. In some instances, special protocols (e.g., mixing several different primitives) are developed for important problems. This is expected to provide more efficient protocols due to insight into the problem domain. Such special protocols, however, can require a manual verification and security proof resulting in inefficiencies in practice.
Current domain-specific programming languages (DSPLs) for secure computation do not adequately address these problems. More particularly, DSPLs are either tied to a specific protocol or enable implementing insecure protocols. On the one hand, if a DSPL is tied to a specific protocol, then the protocol may be manually proven secure independent of the functionality. Such a proof extends to all protocols implemented in the particular DSPL, but the DSPL prevents implementing many special, possibly more efficient protocols. On the other hand, if the DSPL is built upon a generic programming language (e.g., Python, Java), all special protocols can be implemented. However, this still allows the programmer to also implement insecure protocols that do not withstand security verification.